package cwb
import scala.util.parsing.combinator.RegexParsers
import scala.ref.Reference
import scala.collection.mutable.DoubleLinkedList
import agent.Action
import agent.Agent



object Equiv {
  type Graphs = (AgentState, List[AgentState])
      type Block = List[AgentState]
          type Partition = List[Block]

              class Again(p1: List[AgentState], p2: List[AgentState]) extends Exception {
    val newBlock1 = p1
        val newBlock2 = p2
  }

  class Noneqv extends Exception



  def eqCommand(f: Agent => Graphs, in: String): Boolean = {
      val (agent1, agent2) = Agent.parser.getAgentPair(in)


          val agraph = f(agent1)
          val bgraph = f(agent2)
          if (cwb.debug) println ("Got graphs")

          val bool = equiv(agraph, bgraph)
          println(bool)
          bool
  }

  def printGraphs(g: Graphs) {
    println("ROOT " + g._1.printTopLevel())
    for (sub <- g._2) sub.printTopLevel()
  }

  def equiv(agraph: Graphs, bgraph: Graphs): Boolean = {

      if (cwb.debug) {
        println("Size of polygraph map: " + Polygraph.table.size)
        println("GRAPH A: " + agraph._1.keycopy.agentString)
        Polygraph.smartPrint(agraph._2)
        println("GRAPH B: " + bgraph._1.keycopy.agentString)
        println("size " + bgraph._2.size)
        Polygraph.smartPrint(bgraph._2)
        println("in equiv")
      }
      partition(agraph._1, bgraph._1, agraph._2 ++ bgraph._2, true)._1
  }

  /**
   * Partition takes two initial states from two different graphs together with a union
   * of the graph and partitions it. If eqdeciding is set this returns whether the two
   * graphs are equivalent.
   * 
   * @param ast initial state of the first graph
   * @param bst initial state of the second graph
   * @graph union of the graphs
   * @param eqdeciding true iff checking equivalence
   * 
   * @return (partition, equivalence boolean)
   */
  def partition(ast: AgentState, bst: AgentState, graph: List[AgentState], eqdeciding: Boolean): (Boolean, Partition) = {
    if (cwb.debug) {
      println("checking equivalence between " + ast.keycopy.agentString + " and " +
          bst.keycopy.agentString)
          cwb.dbprintln("graph len = " + graph.length)
          Polygraph.smartPrint(graph)
    }


    var blocknum = 1



        def resetPid(state: AgentState) = state.pid = 0

        var parts: Partition = {
      graph.foreach(x => resetPid(x))

      // Ensure all the pids were correctly reset
      graph.foreach(x => assert(x.pid == 0))

      List(graph)
    }

    var result = parts

        // numChecks is used in the exception handling of the Again exception.
        // to figure out where the exception was thrown and how much has already
        // passed equivalence tests.
        var numChecks = 0
        def check(parts: Partition): Unit = {

      if (cwb.debug) println("check called")
      parts match {
      case List() => {
        numChecks = 0
            ()
      }
      case blk::unchecked => {
        numChecks +=1
            var blk1 = blk
            if (cwb.debug) println("Unchecked")

            /**
             * Checkblk is used for checking the equivalence by going over an agent state list
             * representation of the graph.
             */
            def checkblk(glist: List[AgentState]): Unit = {
                glist match {
                case List() => throw Panic("Should not happen, empty list in checkblk!")
                case block@(item::rest) => {
                  var split = false
                      def pnums(lst: List[AgentState]): List[Int] = {
                      // TODO: Efficiency???
                      lst match {
                      case List() => List()
                      case h::t => {
                        var res = List(h.pid)
                            res = res ++ pnums(t)
                            res = res.removeDuplicates
                            res.sort((a,b) => a <= b)
                      }
                      }
                  }

                  def caps(als: List[(Action, List[AgentState])]): List[(Action, List[Int])] = {
                      //var lst: List[(Action, List[Int])] = List()
                      for (al <- als) yield {
                        (al._1, pnums(al._2))
                      }
                  }

                  val cap1 = caps(item.suc)
                      // info not needed, trivtest = true for the infotest in SML.


                      def blockEq(item1: (Action, List[Int]), item2: (Action, List[Int])) = {
                    (item1._1, item1._2, item2._1, item2._2) match {
                    case (act1, int1, act2, int2) => { 
                      val x = (act1 == act2) && int1 == int2
                          x
                    }
                    }
                  } 

                  /**
                   * A capability is like a successor list, but contains the
                   * block number of the target states rather than the states.
                   * Thus, when checking for a bisimulation it is sufficient
                   * to compare capabilities.
                   * @param items1 first block to check for capability equivalence
                   * @param items2 second block to check for capability equivalence
                   * @return items1 capability == items2 capability.
                   */
                  def capaEq(items1: List[(Action, List[Int])], items2: List[(Action, List[Int])]): Boolean = {

                    (items1, items2) match {
                    case (List(), List()) => if (cwb.debug) println("empty capaeq"); true
                    case (List(), _) => false
                    case (_, List()) => false
                    case (a::as, b::bs) => if (!blockEq(a,b)) false else capaEq(as,bs)
                    }

                  }

                  /**
                   * checkState verifies whether the given agent state is capability equivalent to
                   * the currently checked agent state and if not marks the state and sets partition
                   * to perform a split.
                   * @param state agent state to be capability checked against the current state.
                   */
                  def checkstate(state: AgentState) = {
                    val x = cap1
                        val y = caps(state.suc)
                        if (capaEq(x,y)) {
                          if (cwb.debug) println("Capa eq = true")
                        } else {
                          if (cwb.debug) println("Capa eq = false")

                          state.mark = true
                          split = true
                        }
                  }

                  def newBlocks(xs: Block): (List[AgentState], List[AgentState]) = {
                    xs match {
                    case List() => (List(), List())
                    case (h::t) => {
                      val (p1, p2) = newBlocks(t)
                          if (h.mark) {
                            h.mark = false
                                h.pid = blocknum
                                (h::p1, p2)    
                          } else {
                            (p1, h::p2)
                          }
                    }
                    }

                  }
                  rest.foreach(x => checkstate(x))
                  if (split) {
                    val (p1, p2) = newBlocks(block)
                        //blk1 = p2
                        throw new Again(p1, p2)
                  }
                }


                }

            }
        checkblk(blk1)
        check(unchecked)

      }
      }

    }

    /**
     * equiv takes two graphs and returns whether they are equivalent
     * @param g1 the first (initial, full graph)
     * @param g2 the second (initial, full graph)
     * @return g1 equivalent to g2
     */
    def equiv(g1: Graphs, g2: Graphs): Boolean = {
      (g1._1, g1._2, g2._1, g2._2) match {
      case (a, graph1, b, graph2) => {
        partition(a,b,graph1 ++ graph2, true)._1 
      }
      }
    }


    def iterate(parts: Partition): Unit = {
      // Reset current position.
      numChecks = 0
          try {
            check(parts)
          } catch {
          case e: Again => {
            if (cwb.debug) {
              println("again")          
              println("p1 " + ast.pid)
              println("p2 " + bst.pid)
            }
            if (eqdeciding && ast.pid != bst.pid) {
              throw new Noneqv()
            } else {
              blocknum += 1
                  result = e.newBlock1::e.newBlock2::(parts.drop(numChecks))
                  return iterate(result)
            }
          }
          }
    }
    try {            
      iterate(parts)
      (true, result)
    } catch {
    case e: Noneqv => (false, null)
    }
  }

}

object StrongEqCommand extends Command {
  val name = "strongeq"
      val helpShort = "are two agents strongly bisimilar?"
      val helpDetailed = "strongeq(A,B);\n\nReturns true iff A and B are related by some strong bisimulation. " +
          "\nR is a strong bisimulation iff PRQ implies " +
          "\nwhenever P -a-> P' there exists Q' st Q -a-> Q' and P' R Q' and " +
          "\nwhenever Q -a-> Q' there exists P' st P -a-> P' and P' R Q'." +
          "\n\nSee also: eq"

  /**
   * Parses the given string into two agent graphs and displys whether these are strongly
   * bisimular.
   */
   def apply(input: String) = {
    Equiv.eqCommand(Polygraph.SGraph, input)
  }
}

object EqCommand extends Command {
  val name = "eq"
      val helpShort = "are two agents observationally equivalent (weakly bisimilar)?"
      val helpDetailed = "eq(A,B);" +
          "\n" +
          "\nReturns true iff the agents are related by some weak bisimulation." +
          "\nR is a weak bisimulation iff PRQ implies" +
          "\n" +
          "\nwhenever P -a-> P' there exists Q' st Q =^a=> Q' and P' R Q' and" +
          "\n" +
          "\nwhenever Q -a-> Q' there exists P' st P =^a=> P' and P' R Q'." +
          "\n" +
          "\nSee also: strongeq"

   /**
    * Parses the given string into two agent graphs and displys whether these are weakly
    * bisimular.
    */
    def apply(input: String) = {
    Equiv.eqCommand(Polygraph.WGraph, input)
  }
}

